feat(Analysis): add Commute.exp_smul_right and symmetric variants#39723
feat(Analysis): add Commute.exp_smul_right and symmetric variants#39723VictorBoscaro wants to merge 1 commit into
Conversation
Adds Commute.exp_smul_right, Commute.exp_smul_left, and Commute.exp_smul to Mathlib/Analysis/Normed/Algebra/Exponential.lean, completing the Commute.exp_* × Commute.smul_* cross product. Each is a one-line composition of existing lemmas. The typeclass scope matches the existing Commute.exp_right family verbatim.
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 0bcf97ceb9Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
eric-wieser
added
the
LLM-generated
|
We appreciate your desire to contribute to mathlib. Unfortunately, this PR does not meet community standards. Our reviewer time is very limited so we must prioritize both individuals who can learn and contribute back to the community and sufficiently high quality content as to make the process smooth and valuable. |
2 participants
Summary
Adds
Commute.exp_smul_right,Commute.exp_smul_left, andCommute.exp_smulto
Mathlib/Analysis/Normed/Algebra/Exponential.lean, immediately afterCommute.exp. One-line compositions ofCommute.smul_*withCommute.exp_*.Same typeclass scope as
Commute.exp_right; no new hypotheses.Context
Commute.exp_right/Commute.exp_left/Commute.exphandle theCommute x (exp y)shape;Commute.smul_right/Commute.smul_lefthandleCommute x (r • y). The natural compositionCommute x (exp (r • y))—the canonical shape in one-parameter semigroups
t ↦ exp (t • Q)— is absentand currently requires inline chaining.
Notes
Commute.exp_right.@[simp]/ no@[to_additive]— matches the existingCommute.exp_*choices.exp_smul_self,exp_nsmul_*can follow separately if needed.Where this can be used
Existing Mathlib — concrete simplifications.
Mathlib/Analysis/SpecialFunctions/Exponential.lean:292, 313write the chainexplicitly:
(((Commute.refl x).smul_left t').smul_right t).exp_rightwouldcompress to
((Commute.refl x).smul_left t').exp_smul_right t.Mathlib/Analysis/CStarAlgebra/Fuglede.lean:76usesgrind [exp_add_of_commute, Commute.smul_right, Commute.neg_right]to dischargea commutation goal in the Fuglede–Putnam–Rosenblum proof; these lemmas would be
natural additions to that hint set.
Areas where this composition recurs.
The composition
[P, Q] = 0 ⟹ [P, exp(t · Q)] = 0appears in:Pcommutes with the infinitesimal generatorQ⟹Pcommutes withe^{tQ}.U(t) = exp(itA); commuting observables commute with the full evolution.M_t = exp(tQ)forQa Q-matrix; symmetries ofQlift to symmetries ofM_t.X,Ycommuting in the Lie algebra ⟹exp(tX),exp(sY)commute.f(A)g(A) = g(A)f(A)for commuting operators, with the exp specialisation at each step.exp(t·Δ)/exp(-itH).σ^φ_t = Ad(Δ^{it})on a von Neumann algebra.